;(set-option :produce-proofs true)
(set-option :produce-interpolants true)
(set-logic QF_LRA)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (! (>= x 0) :named p1))
(assert (! (>= y 0) :named p2))
(push 1)
(assert (! (>= (- 10) (+ x y)) :named p3))
(check-sat)
(get-interpolants p1 (and p2 p3))
(pop 1)
(push 1)
(assert (! (>= a x) :named p4))
(assert (! (>= b y) :named p5))
(assert (! (>= (- 20) (+ a b)) :named p6))
(check-sat)
(get-interpolants (and p1 p4 p6) (and p2 p5))
